COMMENT ⊗   VALID 00021 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	facts about nth, nthcdr and fstposition
C00005 00003	shouldn't be needed
C00007 00004	forms of doubleinduction
C00013 00005	basic facts about nth
C00023 00006	nthcdr
C00026 00007	fstposition
C00028 00008	lists regarded as sets
C00032 00009	facts about allp
C00034 00010	* forms of doubleinduction
C00049 00011	basic facts about nth
C00051 00012	member_nth
C00061 00013	proofs of other facts needed verification of facts about nthcdr
C00068 00014	nthcdr_induction1 and nthcdr_induction
C00077 00015	facts about fstposition                   
C00082 00016	lemmata nth_fstposition and fstposition_nth
C00087 00017	less effective proof:
C00092 00018	proof of facts about sets                             
C00094 00019	proof of properties of mkset,mklset                    ***bug***
C00101 00020	mklset_un                                             
C00102 00021	proofs allp
C00112 ENDMK
C⊗;
;facts about nth, nthcdr and fstposition
(wipe-out)
(get-proofs length)

;now we need to tie up natural numbers and s-expressions
 
(axiom |∀n.¬null(n)|)
(label simpinfo)

(axiom |∀n.sexp n|)
(label simpinfo)
;shouldn't be needed
;(proof length)

;(axiom |∀u n.n<length(u)⊃¬null u|)
;(label simpinfo)

;although if u is null then "n<length(u)" rewrites to FALSE,
;ekl does not give this in one step

;forms of doubleinduction
(proof listinduction)

;a convenient form for double induction on lists

(axiom |∀phi2.(∀u v x y.phi2(nil,u)∧phi2(u,nil)∧(phi2(u,v)⊃phi2(x.u,y.v)))⊃(∀u v.phi2(u,v))|)
(label doubleinduction)

;the next principle gives a form of double induction for lists and numbers

(axiom |∀phi3.(∀u n x.phi3(nil,n)∧phi3(u,0)∧(phi3(u,n)⊃phi3(x.u,n')))⊃(∀u n.phi3(u,n))|)
(label doubleinduction1)

;basic facts about nth
(proof nth)

;1
(decl nth (syntype: constant) (type: |ground⊗ground→ground|))

;(define nth |∀x u n.nth(x.u,n)= if n=0 then x else nth(u,pred(n))|
;	(use listinductiondef))
;(label simpinfo) (label nthdef)

;2
(defax  nth |∀x u n.nth(nil,n)=nil∧nth(u,0)=car u∧
                    nth(x.u,n')=nth(u,n)|)
(label simpinfo) (label nthdef)
;(define nth |∀x u n.nth(x.u,n)= if n=0 then x else nth(u,pred(n))|
;	(use listinductiondef))

;well-definedness of nth 

;3
(axiom |∀u n.sexp nth(u,n)|)
(label simpinfo)(label sexp_nth)

;membership of nth in the original list

;4
(axiom |∀u n.n<length u⊃member(nth(u,n),u)|)
(label nthmember)

;we need a converse of nthmember

;5
(axiom |∀u y.member(y,u)⊃(∃n.n<length u∧nth(u,n)=y)|)
(label member_nth)

;nthcdr
(proof nthcdr)

;1
(decl nthcdr (syntype: constant) (type: |ground⊗ground→ground|))

;2
(defax  nthcdr |∀x u n.nthcdr(nil,n)=nil∧nthcdr(u,0)=u∧
          		      nthcdr(x.u,n')=nthcdr(u,n)|)
(label simpinfo) (label nthcdrdef)

;3
(axiom |∀u n.listp nthcdr(u,n)|)
(label simpinfo)

;4
;nth nthcdr zero

(axiom |∀u.0<length u⊃nth(u,0).nthcdr(u,1)=u|)
(label nth_nthcdr_zero)

;5
;car nthcdr

(axiom |∀u n.n<length u⊃car nthcdr(u,n)=nth(u,n)|)
(label car_nthcdr)

;6
;cdr nthcdr

(axiom |∀u n.cdr nthcdr(u,n)=nthcdr(u,n')|)
(label cdr_nthcdr)

;7
;nthcdr car cdr

(axiom |∀u n.n<length u⊃nthcdr(u,n)=nth(u,n).nthcdr(u,n')|)
(label nthcdr_car_cdr)

;8
;nth in nthcdr

(axiom |∀u n m.n≤m∧m<length u⊃member(nth(u,m),nthcdr(u,n))|)
(label nth_in_nthcdr)

;9
;nth nthcdr

(axiom |∀u n m.n<length u∧m<length (nthcdr(u,n))⊃nth(nthcdr(u,n),m)=nth(u,m+n)|)
(label nth_nthcdr)

;10
;length nthcdr

(axiom |∀u n.n≤length u⊃length (nthcdr(u,n))=length u-n|)
(label length_nthcdr)

;11
(axiom |∀u.nthcdr(u,length u)=nil|)
(label last_nthcdr)

;12
(axiom |∀u n.length(u)≤n⊃nthcdr(u,n)=nil|)
(label trivial_nthcdr)

;13
(axiom |∀a u n.allp(a,u)⊃allp(a,nthcdr(u,n))|)
(label allp_nthcdr)

;local listinduction, using nth and nthcdr

;14
(axiom |∀phi4 u.phi4(nil,length u)∧
 (∀n.n<length u∧phi4(nthcdr(u,n'),n')⊃phi4(nth(u,n).nthcdr(u,n'),n))⊃phi4(u,0)|)
(label nthcdr_induction1)

;15
(axiom |∀phi u.phi(nil)∧(∀n.n<length(u)⊃
               (phi(nthcdr(u,n'))⊃phi(nth(u,n).nthcdr(u,n'))))⊃phi(u)|)
(label nthcdr_induction)
;fstposition
(proof fstposition)

(decl (fstposition) (type: |ground⊗ground→ground|))
(define fstposition |∀x u y.fstposition(nil,y)=nil∧
			fstposition(x.u,y)=if ¬member(y,x.u) then nil else
		                        if x=y then 0 else add1(fstposition(u,y))|
					listinductiondef)
(label fstpositiondef)

(axiom |∀u y.(null fstposition(u,y)⊃¬member(y,u))∧
             (member(y,u)⊃natnum(fstposition(u,y)))∧
             (null fstposition(u,y)∨natnum(fstposition(u,y)))|)
(label simpinfo)(label posfacts)

(axiom |∀u y.sexp fstposition(u,y)|)
(label simpinfo)(label sortpos)

(axiom |∀u y.member(y,u)⊃fstposition(u,y)<length u|)
(label pos_length)

(axiom |∀u n.member(n,u)⊃nth(u,fstposition(u,n))=n|)
(label nth_fstposition)

(axiom |∀u n.uniqueness(u)∧member(n,u)⊃fstposition(u,nth(u,n))=n|)
(label fstposition_nth)

;lists regarded as sets
(proof sets)

(decl mklset (type: |ground→@set|))
(define mklset |∀u.mklset(u)=λx.member(x,u)|)
;(define mklset |∀u.mklset(u)=λxv.member(xv,u)|)
(label mklsetdef)

;facts about sets: mkset, mklset and union

(axiom |∀u y.member(y,u)⊃mkset(y)⊂mklset u|)
(label mkset_mklset)

(axiom |∀u.mklset(u)=(λx.(∃k.k<length u∧nth(u,k)=x))|)
;(axiom |∀u.mklset(u)=(λxv.(∃k.k<length u∧nth(u,k)=xv))|)
(label mklset_fact)

;facts about mkset, mklset and union
(proof unionfacts)

(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λx.(∃k.k<n∧nth(u,k)=x))|)
;(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λxv.(∃k.k<n∧nth(u,k)=xv))|)
(label mksetfact)

(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λx.(mklset(u))(x))|)
;(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λxv.(mklset(u))(xv))|)
(label mklset_un)

;facts about allp
(proof allp)
;the following formulation of the definition of allp is more convenient when
;deriving instead of rewriting

;allpfact

;(trw |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)| (open allp))
;∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)

(axiom |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)|)
(label allpfact)

(axiom |∀phi1 u.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
(label allp_introduction)

(axiom |∀phi1 x u.member(x,u)∧allp(phi1,u)⊃phi1(x)|)
(label allp_elimination)

(axiom |∀u a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|)
(label allp_implication)

(axiom |∀phi1 u.(∀n.n<length u⊃phi1(nth(u,n)))⊃allp(phi1,u)|)
(label nth_allp)

(save-proofs nth)
;* forms of doubleinduction
;time 9s
(wipe-out)
(get-proofs nth)

(proof listinduction)

;a useful principle which follows from listinduction
;corresponds to a proof by cases arguments

(trw |∀phi.(phi(nil)∧∀x u.phi(x.u))⊃∀u.phi(u)| listinduction)
;∀PHI.PHI(NIL)∧(∀X U.PHI(X.U))⊃(∀U.PHI(U))
(label listcases)
 
;the next principle gives a convenient form for double induction on lists

(assume |∀u v x y.phi2(nil,u)∧phi2(u,nil)∧(phi2(u,v)⊃phi2(x.u,y.v))|)
(label dindass)

(ue (phi |λu.∀v.phi2(u,v)|) listinduction
    (use dindass) (use listcases ue: ((phi.|λv.phi2(x.u,v)|)) ))
;∀U V.PHI2(U,V)
;deps: (DINDASS)

(ci (dindass) *)
;(∀U V X Y.PHI2(NIL,U)∧PHI2(U,NIL)∧(PHI2(U,V)⊃PHI2(X.U,Y.V)))⊃(∀U V.PHI2(U,V))
(label doubleinduction)
 
;the next principle gives a form of double induction for lists and numbers
 
(assume |∀u n x.phi3(nil,n)∧phi3(u,0)∧(phi3(u,n)⊃phi3(x.u,n'))|)
(label dindass1)

(ue (phi |λu.∀n.phi3(u,n)|) listinduction
    (use dindass1) (use proof_by_induction ue: ((a.|λn.phi3(x.u,n)|)) ))
;∀U N.PHI3(U,N)
;deps: (DINDASS1)

(ci (dindass1) *)
;(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))
(label doubleinduction1)

;basic facts about nth
;15s
(wipe-out)
(get-proofs nth)
(proof nth)

;prove by double induction the well-definedness of nth for the obvious range

;3
(unlabel simpinfo sexp_nth have_member have_member1)

(ue (phi3 |λu n.sexp nth(u,n)|) doubleinduction1 (open nth))
;∀U N.SEXP NTH(U,N)

(label simpinfo sexp_nth)

;4
;prove by double induction the membership of nth in the original list
(ue (phi |λu.0<length u⊃member(nth(u,0),u)|) listinduction
    (open length nth member))
;∀U.0<LENGTH U⊃MEMBER(NTH(U,0),U)

(ue (phi3 |λu n.n<length u ⊃ member(nth(u,n),u)|) doubleinduction1
    (open length nth) (use memberdef mode: always)(use *))
;∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)
(label nthmember)

;member_nth
(wipe-out)
(get-proofs nth)
(proof member_nth)

(assume |(member(y,u)⊃(∃n.n<length u∧nth(u,n)=y))|)
(label m_n1)

(assume |y=x|)
(label m_n2)

(trw |0<length(x.u)∧nth(x.u,0)=y| (open nth) *)
;0<LENGTH (X.U)∧NTH(X.U,0)=Y

(derive |∃n.n<length(x.u)∧nth(x.u,n)=y| *)
(label m_n3)

(assume |member(y,u)|)

(define nv |nv<length u∧nth(u,nv)=y| (m_n1 *))

(trw |nv'<length(x.u)∧nth(x.u,nv')=y| (open nth) * )
;NV'<LENGTH (X.U)∧NTH(X.U,NV')=Y

(derive |∃n.n<length(x.u)∧nth(x.u,n)=y| *)
(label m_n4)

(assume |member(y,x.u)| )
(label m_n5)

(rw * (open member))
;Y=X∨MEMBER(Y,U)

(cases * m_n3 m_n4)
;∃N.N<LENGTH (X.U)∧NTH(X.U,N)=Y

(ci m_n5)
;MEMBER(Y,X.U)⊃(∃N.N<LENGTH U'∧NTH(X.U,N)=Y)

(ci m_n1)

(ue (phi |λu.member(y,u)⊃(∃n.n<length u∧nth(u,n)=y)|) listinduction 
   (open member nth) *)
;∀U.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)
;proofs of other facts needed; verification of facts about nthcdr

(wipe-out)
(get-proofs nth)
(proof nthcdr)
;3
(unlabel simpinfo nthcdr#3)

(ue (phi3 |λu n.listp nthcdr(u,n)|) doubleinduction1
    (open nthcdr) )
(label simpinfo nthcdr#3)
;∀U N.LISTP NTHCDR(U,N)


;4
;nth_nthcdr_zero

(ue (phi |λu.0<length u⊃nth(u,0).nthcdr(u,0')=u|) listinduction 
    (open length nth nthcdr))
;∀U.0<LENGTH U⊃NTH(U,0).NTHCDR(U,1)=U


;5
;car_nthcdr


(ue (phi3 |λu n.n<length(u)⊃car(nthcdr(u,n))=nth(u,n)|) doubleinduction1
    (open length nthcdr nth))
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)


;7
;cdr_nthcdr


(ue (phi |λu.cdr(nthcdr(u,0))=nthcdr(u,0')|) listinduction
    (open nthcdr))
;∀U.CDR U=NTHCDR(U,1)

(ue (phi3 |λu n.cdr(nthcdr(u,n))=nthcdr(u,n')|) doubleinduction1   
    (open nthcdr) *)
;∀U N.CDR NTHCDR(U,N)=NTHCDR(U,N')


;8 
;nthcdr_car_cdr


(ue (phi |λu.0<length(u)⊃nthcdr(u,0)=nth(u,0).nthcdr(u,0')|) listinduction
	( car_nthcdr cdr_nthcdr))
;∀U.0<LENGTH U⊃U=CAR U.NTHCDR(U,1)

(ue (phi3 |λu n.n<length(u)⊃nthcdr(u,n)=nth(u,n).nthcdr(u,n')|) doubleinduction1
	(open length)(use car_nthcdr cdr_nthcdr) *)
;∀U N.N<LENGTH U⊃NTHCDR(U,N)=NTH(U,N).NTHCDR(U,N')


;10
;last_nthcdr


(ue (phi |λu.nthcdr(u,length(u))=nil|) listinduction
    (open nthcdr))
;∀U.NTHCDR(U,LENGTH U)=NIL


;11
;nth in nthcdr 

(assume |∀M.(N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))|)
(label nincdr1)

(ue (a |λM.(N'<M∧M<LENGTH(X.U)⊃MEMBER(NTH(X.U,M),NTHCDR(X.U,N')))|) proof_by_induction
        (part 2(nuse nthdef nthcdrdef lengthdef)) nincdr1 zero_non_less_successor)
;∀N2.N'<N2∧N2<LENGTH (X.U)⊃MEMBER(NTH(X.U,N2),NTHCDR(X.U,N'))
 
(ci NINCDR1)
;(∀M.N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))⊃
;(∀N2.N'<N2∧N2<LENGTH U'⊃MEMBER(NTH(X.U,N2),NTHCDR(U,N)))

(ue (phi3 |λu n.∀m.n<m∧m<length(u)⊃member(nth(u,m),nthcdr(u,n))|) doubleinduction1
     (use nthmember mode: exact) (use * mode: exact))
;(∀U N M.N<M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N)))

(trw |∀u n m.n≤m∧m<length(u)⊃member(nth(u,m),nthcdr(u,n))| (open lesseq member)
     (use normal mode: always)(use * nthcdr_car_cdr mode: exact)) 
;∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))

;13
;trivial_nthcdr

(ue (phi3 |λu n.length(u)≤n⊃nthcdr(u,n)=nil|) doubleinduction1 
    (part 1#1 (open lesseq)))
(label trivial_nthcdr)

;14
;allp_nthcdr

(ue (phi3 |λu n.allp(a,u)⊃allp(a,nthcdr(u,n))|) doubleinduction1 (open allp))
;∀U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))
(label allp_nthcdr)

;15
;nth nthcdr
(ue (phi3 |λu n.n<length u∧m<length(nthcdr(u,n))⊃nth(nthcdr(u,n),m)=nth(u,m+n)|)
     doubleinduction1 )
;∀U N.N<LENGTH U∧M<LENGTH (NTHCDR(U,N))⊃NTH(NTHCDR(U,N),M)=NTH(U,M+N)

;16 
;length nthcdr
(ue (phi3 |λu n.n≤length u⊃length(nthcdr(u,n))=length u-n|) doubleinduction1 
   (use successor_minus mode: always) (open minus)(part 1#1#1 (open lesseq)))
;∀U N.N≤LENGTH U⊃LENGTH (NTHCDR(U,N))=LENGTH U-N

;nthcdr_induction1 and nthcdr_induction
(proof nthcdr_induction)

(assume |∀n.n<length(u)∧phi4(nthcdr(u,n'),n')⊃phi4(nth(u,n).nthcdr(u,n'),n)|)
(label n_i_1)

(derive |∀n.n<length(u)⊃(phi4(nthcdr(u,n'),n')⊃phi4(nthcdr(u,n),n))| *
       (use  nthcdr_car_cdr mode: always))
(label n_i_2)

; two cases

(derive |length(u)≤n∨n<length(u)| trichotomy2)
(label n_i_cases)

;one completely trivial

(assume |length(u)≤n|)
(label n_i_c1)

(trw |length(u)-n=0⊃
	(phi4(nthcdr(u,length(u)-n),length(u)-n)⊃
	 phi4(nthcdr(u,length(u)-n'),length(u)-n'))|(open minus pred) )
(label n_i_3)

(derive |phi4(nthcdr(u,length(u)-n),length(u)-n)⊃
         phi4(nthcdr(u,length(u)-n'),length(u)-n')|
	(n_i_c1 total_subtraction  n_i_3 )) 
(label n_i_case1)

;the other quite trivial too...


(assume |n<length(u)|)
(label n_i_c2)

(ue (n |length(u)-(n')|) n_i_2 )
;LENGTH U-N'<LENGTH U⊃
;(PHI4(NTHCDR(U,(LENGTH U-N')'),(LENGTH U-N')')⊃
; PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N'))

(rw * (use n_i_c2)(use minusfact11 ue: ((n.|length(u)|)) )
            (use minusfact10 mode: exact direction: reverse))
;PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)⊃PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N')
(label n_i_case2)


(cases n_i_cases n_i_case1 n_i_case2)
;PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)⊃PHI4(NTHCDR(U,LENGTH U-N'),LENGTH U-N')

(ue (a |λn.phi4(nthcdr(u,length(u)-n),length(u)-n)|) proof_by_induction *
  (part 1(use last_nthcdr mode: exact)(open minus)) )
(label n_i_5)
;PHI4(NIL,LENGTH U)⊃(∀N.PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N))

(assume |phi4(nil,length(u))|)(label n_i_6)

(derive |∀N.PHI4(NTHCDR(U,LENGTH U-N),LENGTH U-N)| (n_i_5 n_i_6))
(ue (n |length u|) * )
;PHI4(U,0)

;this gives nthcdr_induction1

(ci (n_i_6 n_i_1))
;PHI4(NIL,LENGTH U)∧
;(∀N.N<LENGTH U∧PHI4(NTHCDR(U,N'),N')⊃PHI4(NTH(U,N).NTHCDR(U,N'),N))⊃PHI4(U,0)

;nthcdr_induction follows

(ue ((phi4.|λu n.phi(u)∧n=n|)(u.u)) *)
;PHI(NIL)∧(∀N.N<LENGTH U∧PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N')))⊃PHI(U)

;The principle of nthcdr induction is a trick to reduce induction on lists to finite
;induction on numbers. Assume a list U is given; we can prove that U has a certain
;property PHI from the fact that the null list has property PHI and that if X.V is 
;a tail of U and V has the property PHI then X.V has the property PHI.
;However, using the functions NTH and NTHCDR we can formulate this method of proof
;as finite descent from PHI(NTHCDR(U,LENGTH(U))) to PHI(NTHCDR(U,0)).

;Indeed we prove by induction on N

;∀N.PHI(NTHCDR(U,LENGTH(U)-N)).

;For N=0, NTHCDR(U,LENGTH(U)-N) is NIL, and we have PHI(NIL). 
;Assume  PHI(NTHCDR(U,LENGTH(U)-N)). If N≥LENGTH(U) since subtraction is defined
;as a total function on nonnegative integers we have
;LENGTH(U)-N = 0 = LENGTH(U)-N'
;so the induction step is trivial. If N<LENGTH(U),
;LENGTH(U)-N=(LENGTH(U)-N')' by elementary arithmetic
;and 
;∀K.K<LENGTH(U)⊃ ( NTHCDR(U,K') ⊃ NTHCDR(U,K))
;is the inductive step of our principle, so we can complete the induction step, 
;by letting K to be LENGTH(U)-N' :
;NTHCDR(U,LENGTH(U)-N) ⊃ NTHCDR(U,LENGTH(U)-N')

;Finally it is convenient to write 
;NTHCDR(U,K) as NTH(U,K).NTHCDR(U,K')  (using NTHCDR_CAR_CDR)

;nthcdr_induction1 is a slight generalization, with an extra inductive variable
;facts about fstposition                   
(wipe-out)
(get-proofs nth)

(proof fstpositionprop)
(trw |∀k.¬null k'|) 
(label simpinfo)

(unlabel simpinfo posfacts sortpos)

(ue (phi |λu.(null fstposition(u,y)⊃¬member(y,u))∧
             (member(y,u)⊃natnum fstposition(u,y))∧
             (null fstposition(u,y)∨natnum fstposition(u,y))|) listinduction 
    (part 1 (open member fstposition) (use normal mode: always)))
;∀U.(NULL FSTPOSITION(U,Y)⊃¬MEMBER(Y,U))∧
;   (MEMBER(Y,U)⊃NATNUM(FSTPOSITION(U,Y)))∧
;   (NULL FSTPOSITION(U,Y)∨NATNUM(FSTPOSITION(U,Y)))
(label simpinfo posfacts)

(unlabel simpinfo sortpos)

(ue (phi |λu.∀y.sexp fstposition(u,y)|) listinduction
    (part 1 (open member fstposition) (use normal mode: always)))
;∀U Y.SEXP FSTPOSITION(U,Y)

(label simpinfo sortpos)

;pos_length

(ue (phi |λu.∀y.member(y,u)⊃fstposition(u,y)<length(u)|) listinduction 
    (part 1 (open member fstposition) (use normal mode: always)))
;∀U Y.MEMBER(Y,U)⊃FSTPOSITION(U,Y)<LENGTH U
;lemmata nth_fstposition and fstposition_nth

;lemma nth_fstposition

(ue (phi |λu.∀n.member(n,u)⊃nth(u,fstposition(u,n))=n|) listinduction 
   (use normal mode: always)
    (open member fstposition nth))
;∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N
(label nth_fstposition)

(proof fstposition_nth)
1.  (ue (phi |λu.0<length u⊃fstposition(u,nth(u,0))=0|)
	listinduction (open fstposition nth member))
    ;∀U.0<LENGTH U⊃FSTPOSITION(U,CAR U)=0

2.  (derive |n<length u ∧ x=nth(u,n) ⊃ member(x,u)| (nthmember))

3.  (derive |uniqueness(x.u)∧n<length u⊃¬x=nth(u,n)| * (open uniqueness))

4.  (ue (phi3 |λu n.uniqueness u∧n<length u⊃fstposition(u,nth(u,n))=n|)
	doubleinduction1 *
	(open fstposition nth member uniqueness) -3 nthmember)
    ;∀U N.UNIQUENESS(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N
;less effective proof:

;fstposition_nth, with the hypothesis that U is INJ. 
;UNIQUENESS is defined by recursion, INJ is not.

;lemma fstposition_nth
(proof fstposition_nth)


(ue (phi |λu.0<length(u)⊃fstposition(u,nth(u,0))=0|) listinduction
	(open fstposition nth))
;∀U.0<LENGTH U⊃FSTPOSITION(U,NTH(U,0))=0
(label fstpos_nth0)

(assume |inj(x.u)|)
(label fstpos_nth1)

(rw * (open inj))
(label fstpos_nth2)
;∀N M.N<LENGTH U'∧M<LENGTH U'∧NTH(X.U,N)=NTH(X.U,M)⊃N=M

(ue ((n.|n'|)(m.|m'|)) *)
;N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M

(trw |inj(u)| * (open inj) )

(ci fstpos_nth1)
(label use_indhyp)
;INJ(X.U)⊃INJ(U)

(trw |nth(x.u,0)| (open nth))(label fstpos_nth3)
;NTH(X.U,0)=X

(assume |x=nth(x.u,n')|)(label fstpos_nth4)

(trw |nth(x.u,0)=nth(x.u,n')| (fstpos_nth3 fstpos_nth4)(nuse nthdef))
;NTH(X.U,0)=NTH(X.U,N')
(label fstpos_nth5)

(assume |n<length(u)|)(label fstpos_nth6)
(ue ((n.|0|)(m.|n'|)) fstpos_nth2 fstpos_nth5 fstpos_nth6)
;FALSE

(ci FSTPOS_NTH4)
;¬X=NTH(U,N)

(ci (FSTPOS_NTH1 FSTPOS_NTH6))
;INJ(X.U)∧N<LENGTH U⊃¬X=NTH(U,N)
(label fstpos_nth7)

(ue (phi3 |λu n.inj(u)∧n<length(u)⊃fstposition(u,nth(u,n))=n|) doubleinduction1
   (open fstposition nth) (use fstpos_nth0 use_indhyp fstpos_nth7 mode: exact) )
;∀U N.INJ(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N

;LEMMA
;∀U N.INJ(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N
;Proof:By double induction on U and N. The base case for U=NIL is trivial;
;the one for N=0 is proved by listinduction [line fstpos_nth0]; in the induction
;step the facts that NTH(X.U,0)=X and FSTPOSITION(X.U,X)=0 are used.

;Assume the induction hypothesis;
;INJ(U)∧N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N
;want
;INJ(X.U)∧N'<LENGTH(X.U)⊃FSTPOSITION(X.U,NTH(X.U,N'))=N'
;So assume also INJ(X.U) and N'<LENGTH(X.U) (which rewrites to N<LENGTH(U) ).
;Now FTSPOSITION(X.U,NTH(X.U,N')) rewrites to
;(IF X=NTH(U,N) THEN 0 ELSE FSTPOSITION(U,NTH(U,N))')
;or in other words, we can apply the induction hypothesis only if X does not occur
;in U: here we have to use the fact that X.U is injective, which denies immediately
;the "if" clause .(Indeed assume X=NTH(X.U,N'); since X=NTH(X.U,0) too, by definition
;of INJ we obtain N'=0). To apply the induction hypothesis we need also to show
;that INJ(X.U) implies INJ(U), which is straightforward [line fstpos_nth1].

;facts used
;labels: INJDEF 
;(DEFINE INJ |∀U.INJ(U)=(∀N M.N<LENGTH U∧M<LENGTH U∧APPL(U,N)=APPL(U,M)⊃N=M)| NIL)

;proof of facts about sets                             
(wipe-out)
(get-proofs nth)

(proof setfacts)
;mkset_mklset

(trw |∀u.member(y,u)⊃mkset(y)⊂mklset(u)| 
   (open mkset mklset inclusion)(der))
;∀U.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)

;mklset_fact

(derive |∀x.(mklset(u))(x)≡(∃k.k<length u∧nth(u,k)=x)| 
         (nthmember member_nth) (open mklset))

(ue ((av.|mklset(u)|)(bv.|λx.(∃k.k<length u∧nth(u,k)=x)|))  set_extensionality
    * (open epsilon) )
;MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))

;proof of properties of mkset,mklset                    ***bug***
(proof unionfacts)

;(derive |∃k.k<n∧nth(u,k)=xv⊃(∃k.k<n'∧nth(u,k)=xv)|
;        (transitivity_of_order successor1))

;(derive |XV=NTH(U,N)⊃(∃k.k<n'∧nth(u,k)=xv)| (* successor1))

;(ue (a |λn.n≤length(u)∧(un(λm.mkset nth(u,m),n))(xv)⊃(∃k.k<n∧nth(u,k)=xv)|)
;    proof_by_induction (open un union)(use normal mode: always)
;    (use succ_lesseq_lesseq succ_less_less mode: exact) (use * -2 mode: always))
;LIST STORAGE CAPACITY EXCEEDED
;BKPT GC-LOSSAGE

(proof mkset)
 
(assume |n≤length u∧(un(λm.mkset nth(u,m),n))(xv)⊃(∃k.k<n∧nth(u,k)=xv)|)
(label mks1)

(assume |n'≤length u|)
(label mks2)

(assume |(un(λm.mkset nth(u,m),n'))(xv)|)
(label mks3)

(rw * (open un union emptyset))
;(UN(λM.MKSET(NTH(U,M)),N))(XV)∨(MKSET(NTH(U,N)))(XV)
(label mks4)

(assume |(un(λm.mkset nth(u,m),n))(xv)|)
(label mks5)

(derive |∃k.k<n∧nth(u,k)=xv|(mks1 * mks2 succ_lesseq_lesseq))

(derive |∃k.k<n'∧nth(u,k)=xv|(* transitivity_of_order successor1))
(label mks6)

(assume |(mkset nth(u,n))(xv)|)
(label mks7)

(rw * (open mkset))
;XV=NTH(U,N)
(derive |∃k.k<n'∧nth(u,k)=xv| (* successor1))

(cases mks4 mks6 *)
;∃K.K<N'∧NTH(U,K)=XV
;deps: (MKS1 MKS2 MKS3)

(ci (mks2 mks3))
;N'≤LENGTH U∧(UN(λM.MKSET(NTH(U,M)),N'))(XV)⊃(∃K.K<N'∧NTH(U,K)=XV)

(ci mks1)

(ue (a |λn.n≤length u∧(un(λm.mkset nth(u,m),n))(xv)⊃(∃k.k<n∧nth(u,k)=xv)|)
   proof_by_induction (part 1#1(open un emptyset)) *)
;∀N.N≤LENGTH U∧(UN(λM.MKSET(NTH(U,M)),N))(XV)⊃(∃K.K<N∧NTH(U,K)=XV)
(label mks8)

;the other direction is trivial

(assume |∃k.k<n∧nth(u,k)=xv|)
(label mks11)

(define kv |kv<n∧nth(u,kv)=xv| *)
(label mks12)

(ue ((setseq.|λk.mkset nth(u,k)|)(m.|kv|)(n.|n|)) unionfact1 (open inclusion))
;KV<N⊃(∀XV.(MKSET(NTH(U,KV)))(XV)⊃(UN(λK.MKSET(NTH(U,K)),N))(XV))
(label mks13)

(trw |(mkset nth(u,kv))(xv)| (open mkset) mks12)
;(MKSET(NTH(U,KV)))(XV)

(derive |(un(λk.mkset(nth(u,k)),n))(xv)|(mks13 mks12 *))
;deps: (MKS12)

(ci mks11)
;(∃K.K<N∧NTH(U,K)=XV)⊃(UN(λK.MKSET(NTH(U,K)),N))(XV)

(derive |∀n.n≤length u∧(un(λm.mkset nth(u,m),n))(xv)≡(∃k.k<n∧nth(u,k)=xv)|(mks8 *))
;mklset_un                                             

(ue (n |length u|) mksetfact 
    (use mklset_fact mode: exact direction: reverse) (open lesseq))
;∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=(λX.(MKLSET(U))(XV))
 
;proofs allp

;allpfact

(trw |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)| (open allp))
;∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)

;allp_introduction

(ue (phi |λu.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
 listinduction (open allp member) (use normal mode: always))
;∀U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)

;allp_elimination

(ue (phi |λu.member(x,u)∧allp(phi1,u)⊃phi1(x)|) listinduction 
    (part 1 (open member allp) (use normal mode: always)))
(label allp_elimination)
;∀U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)

;allp_implication

(ue (phi |λu.∀a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|) listinduction (open allp))
(label allp_implication)
;∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)

;nth_allp

(assume |∀n.n<length(u)⊃phi1(nth(u,n))|)(label allp_intr1)
(ue ((phi.|λu.allp(phi1,u)|)(u.u)) nthcdr_induction (open allp) (use * mode: always))
;ALLP(PHI1,U)
(ci allp_intr1)
;(∀N.N<LENGTH U⊃PHI1(NTH(U,N)))⊃ALLP(PHI1,U)